module models/examples/tutorial/filesystem

// A file system object in the file system
sig FSObject {
  parent: lone Dir
}

// A directory in the file system
sig Dir extends FSObject {
  contents: set FSObject
}

// A directory is the parent of its contents
fact defineContents { 
  all d: Dir, o: d.contents | o.parent = d
}

// A file in the file system
sig File extends FSObject {}

// All file system objects are either files or directories
fact fileDirPartition {
  File + Dir = FSObject
}

// There exists a root
one sig Root extends Dir {
}{
  no parent
}

// File system is connected
fact fileSystemConnected {
  FSObject in Root.*contents
}

// The contents path is acyclic
assert acyclic {
  no d: Dir | d in d.^contents
}

check acyclic for 10

// File system has one root
assert oneRoot {
  one d: Dir | no d.parent
}

check oneRoot for 5

// Every fsobject is in at most one directory
assert oneLocation {
  all o: FSObject | lone d: Dir | o in d.contents
}

check oneLocation for 5


 //an assertion with a counterexample
  assert Wrong {
    all o,p: (FSObject - Root) | (o.parent = p.parent)
  }

 check Wrong for 3
